#define t ConsistencyRT  
#define p IniRunningRT  
#define q IniCommitRT  
#define r ResRunningRT  
#define s ResCommitRT  
#define N 5   //key chain capacity 
bit ConsistencyRT=1; 
bit IniRunningRT = 0; 
bit IniCommitRT = 0; 
bit ResRunningRT = 0; 
bit ResCommitRT = 0; 


//阅读器和标签密钥
byte readerKeySet[N]=255; 
byte tagKey_ver=0; 
byte readerKey_use=3;
int ava_pointer=-1;   //a key index 
byte I=0;      //a loop index 


//for 循环 
#define for()  \
         I = 0; \ 
         do  \
         :: ( I > N-1 ) ->break  \
         :: else ->  
 #define rof()  \
          ; I++  \
         od 


// 宏定义更新 RunningAB   ResRunningAB....的值 
#define IniRunning(x,y)   if   \  
   :: ((x==Reader) && (y==Tag)) -> IniRunningRT=1  \
   :: else skip   \
fi 

#define IniCommit(x,y)  if     \
   :: ((x==Reader) && (y==Tag)) -> IniCommitRT=1  \
   :: else skip    \
   fi
 
#define ResRunning(x,y)  if     \
   :: ((x==Reader) && (y==Tag)) -> ResRunningRT=1  \
   :: else skip   \ 
   fi 
#define ResCommit(x,y)  if    \ 
   :: ((x==Reader) && (y==Tag)) -> ResCommitRT=1  \
   :: else skip   \ 
   fi 



//宏定义攻击者知识库更新 
#define k1(x1)  if   \ 
   :: (x1 == A) -> kA = 1    \
   :: (x1 == B) -> kB = 1    \
   :: (x1 == C) -> kC = 1    \
   :: (x1 == D) -> kD = 1   \
:: (x1 == E) -> kE = 1    \
   :: else skip     \
   fi 
#define k2(x1,x2,x3,x4,x5)  if    \
   :: (x1 == Tag && x2==A && x3==B && x4==Key) -> k_A_B__Key = 1    \
   :: (x1 == Tag && x2==D && x3==E && x4==Key) -> k_D_E__Key = 1    \
   :: else skip     \
   fi 
#define k3(x1,x2,x3,x5)  if    \
   :: (x1 == Reader && x2==C && x3==Key) -> k_C__Key = 1    \
   :: else skip     \
   fi 
#define k4(x1,x2,x3,x4)  if    \
   :: (x1 == Tag && x2==A && x3==B && x4==Key) -> k_A_B__Key_stage2 =1  \
:: (x1 == Tag && x2==D && x3==E && x4==Key) -> k_D_E__Key_stage2= 1   \
   :: else skip     \
   fi 
#define k5(x1,x2,x3) if    \
   :: (x1 == Reader && x2==F && x3==Key) -> k_C__Key_stage2= 1    \
   :: else skip     \
   fi 



//假名与密钥更新 
#define Update(x,y,z) for ()     if     \
   ::  (z==Reader  &&  readerKeySet[I]==255  &&  I!=0)  ->  readerKeySet[I]=readerKeySet[I-1]+1;break    \
   :: (z==Tag)-> tagKey_ver ++;break  \
   :: else skip    \
   fi    \
   rof()



//检查阅读器与标签密钥信息 
inline Find_index()   { 
    d_step{ 
for ()                           
     if  
  ::(readerKeySet[I]!=255&&tagKey_ver==readerKeySet[I])->ava_pointer=I ;break ; 
  ::else skip   
  fi    
   rof() 
 
  } 
} 



//检查阅读器与标签密钥信息 
#define CheckConsistency()    Find_index() ;   \                       
       if   \
   ::( ava_pointer==-1)->ConsistencyRT =0  \
   ::else skip   \
fi    
 


//阅读器端选择密钥 
#define ChooseKey()    for ()    \                           
        if      \
   ::(tagKey_ver==readerKeySet[I])->readerKey_use=readerKeySet[I] ; break  \
   ::else skip    \
        fi  \
   rof() 
 
 
mtype={Reader,Tag,A,B,C,D,E,Key,gD,R}; 
chan ca = [0] of {mtype, mtype, mtype, mtype,byte}; 
chan cb = [0] of {mtype, mtype, mtype,byte}; 
proctype PIni (mtype self;mtype party;mtype msg1;mtype msg2){ 
mtype g1; 
  atomic{ 
  ChooseKey(); 
  IniRunning(self,party);
ca !party, msg1, msg2,Key,readerKey_use 
  } 
  atomic{ 
  ChooseKey(); 
  cb ? eval(self),g1, eval(Key),eval(readerKey_use); 
  Update(IDS,Key,Reader); 
  IniCommit(self,party); 
  ca ! party, D, E,Key,readerKey_use; 
  
  } 
  atomic{ 
  ChooseKey(); 
  IniRunning(self,party); 
  ca !party, msg1, msg2,Key,readerKey_use; 
  } 
  atomic{
ChooseKey(); 
  cb ? eval(self),g1, eval(Key),eval(readerKey_use); 
  Update(IDS,Key,Reader); 
  IniCommit(self,party); 
  ca ! party, D, E,Key,readerKey_use; 
  } 
 
} 
 
proctype PRes (mtype self;mtype party;mtype msg){ 
  mtype g1; 
  mtype g2; 
  atomic{ 
  ca ?eval(Tag),eval(A), eval(B),eval(Key),eval(tagKey_ver); 
  ResRunning(party,self); 
  cb ! party,msg,Key,tagKey_ver; 
  } 
  atomic{
ca ? eval(self), eval(D), eval(E), eval(Key),eval(tagKey_ver); 
  Update(IDS,Key,Tag); 
  ResCommit(party,self); 
  } 
  atomic{ 
  ca ?eval(Tag),eval(A), eval(B),eval(Key),eval(tagKey_ver); 
  cb ! party,C,Key,tagKey_ver; 
  } 
  atomic{ 
  ca ? eval(self), eval(D), eval(E), eval(Key),eval(tagKey_ver); 
  Update(IDS,Key,Tag); 
  ResCommit(party,self); 
  } 
} 


//攻击者进程 
proctype PI() {
mtype x1=0;mtype x2=0; 
  mtype x3=0;mtype x4=0;byte   x5=0; 
  bit kA = 0;bit kB = 0;bit kC = 0; 
  bit kD = 0;bit kE = 0; 
  bit k_Key=0;bit k_A_B__Key = 0;bit k_C__Key = 0; 
  bit k_D_E__Key =0; 
  do 
  ::   ca ! ((kA && k_Key) -> Tag:R), A, A, Key,0 
  ::   ca ! (((kA && kB && k_Key) || k_A_B__Key) -> Tag:R), A, B, Key,0 
  ::   ca ! ((kA && kC && k_Key) -> Tag:R), A, C, Key,0 
  ::   ca ! ((kA && kD && k_Key ) -> Tag:R), A, D, Key,0 
  ::   ca ! ((kA && kE && k_Key) -> Tag:R), A, E, Key,0 
  ::   ca ! ((kA && k_Key) -> Tag:R), A, gD, Key,0 
  ::   ca ! ((kB && kA &&k_Key) -> Tag:R), B, A, Key,0 
  ::   ca ! ((kB && k_Key) -> Tag:R), B, B, Key,0 
  ::   ca ! ((kB && kC && k_Key) -> Tag:R), B, C, Key,0 
  ::   ca ! ((kB && kD && k_Key) -> Tag:R), B, D, Key,0 
  ::   ca ! ((kB && kE && k_Key) -> Tag:R), B, E, Key,0
::   ca ! ((kB && k_Key) -> Tag:R), B, gD, Key,0 
  ::   ca ! ((kC && kA && k_Key) -> Tag:R), C, A, Key,0 
  ::   ca ! ((kC && kB && k_Key) -> Tag:R), C, B, Key,0 
  ::   ca ! (((kC && k_Key) || k_A_B__Key) -> Tag:R), C, C, Key,0 
  ::   ca ! ((kC && kD && k_Key) -> Tag:R), C, D, Key,0 
  ::   ca ! ((kC && kE && k_Key) -> Tag:R), C, E, Key,0 
  ::   ca ! ((kC && k_Key) -> Tag:R), C, gD, Key,0 
  ::   ca ! ((kD && kA && k_Key) -> Tag:R), D, A, Key,0 
  ::   ca ! ((kD && kB && k_Key) -> Tag:R), D, B, Key,0 
  ::   ca ! ((kD && kC && k_Key) -> Tag:R), D, C, Key,0 
  ::   ca ! ((kD && k_Key) -> Tag:R), D, D, Key,0 
  ::   ca ! (((kD && kE && k_Key) || k_D_E__Key) -> Tag:R), D, E, Key,0 
  ::   ca ! ((kD && k_Key) -> Tag:R), D, gD, Key,0 
  ::   ca ! ((kE && kA && k_Key) -> Tag:R), E, A, Key,0 
  ::   ca ! ((kE && kB && k_Key) -> Tag:R), E, B, Key,0    ::   ca ! ((kE && kC && k_Key) -> Tag:R), E, C, Key,0
::   ca ! ((kE && kD && k_Key) -> Tag:R), E, D, Key,0 
  ::   ca ! ((kE && k_Key) -> Tag:R), E, E, Key,0 
  ::   ca ! ((kE && k_Key) -> Tag:R), E, gD, Key,0 
  ::   ca ! ((kA && k_Key)-> Tag:R), gD, A, Key,0 
  ::   ca ! ((kB && k_Key) -> Tag:R), gD, B, Key,0 
  ::   ca ! ((kC && k_Key)-> Tag:R), gD, C, Key,0 
  ::   ca ! ((kD && k_Key) -> Tag:R), gD, D, Key,0 
  ::   ca ! ((kE && k_Key) -> Tag:R), gD, E, Key,0 
  ::   ca ! ( k_Key -> Tag:R), gD, gD, Key,0 
  ::   cb! ((kA && k_Key) -> Reader:R), A, Key,0 
  ::   cb! ((kB && k_Key) -> Reader:R), B, Key,0 
  ::   cb! (((kC && k_Key) || k_C__Key) -> Reader:R), C, Key,0 
  ::   cb! ((kD && k_Key) -> Reader:R), D, Key,0 
  ::   cb! ((kE && k_Key) -> Reader:R), E, Key,0 
  ::   cb! ( k_Key -> Reader:R), gD, Key,0 
  :: d_step {//攻击者学习知识,构建知识库 
   ca ? x1,x2,x3,x4,x5; 
   if
:: (k_Key== 1) -> k1(x2);k1(x3) 
   :: else k2(x1,x2,x3,x4,x5) 
   fi; 
   x1=0;x2=0;x3=0;x4=0;x5=0; 
      } 
  :: d_step { 
   cb ? x1,x2,x3,x5; 
   if 
   :: (k_Key == 1) -> k1(x2) 
   :: else k3(x1,x2,x3,x5) 
   fi; 
   x1=0;x2=0;x3=0;x5=0; 
      } 
  ::CheckConsistency() 
  od 
}
init{//初始化各进程 
  readerKeySet[0]=0; 
  atomic{  
  run PIni(Reader,Tag,A,B); 
  run PI(); 
  run PRes (Tag,Reader,C); 
} 
}
